I've rebased and split off the Kronecker delta stuff, generalising it to an arbitrary decidable type where applicable. I'll see about moving things about sums to abelian groups.

@jdchristensen I've generalised sums from rings to abelian groups. However when the sum takes place in a ring, I've kept the lemma names as rng_sum. We could specialise ab_sum to rings with rng_sum however it doesn't seem to be a big issue reusing it for now.

This looks better. It's actually possible to get rid of the ring assumption for most of the material on the Kronecker delta. It could be defined to land in nat, and then we could use the fact that in any abelian group you can multiply by a natural number (which we write as grp_pow). Also, there should be a coercion from nat to any ring R, and applying the coercion followed by multiplying in R is the same as grp_pow in the underlying abelian group. So then we'd be able to use lemmas like rng_sum_kronecker_delta_l in any abelian group. But maybe this would just make practical usage of this trickier?

Feel free to either merge as is, or to try changing the Kronecker delta to land in nat, whichever you prefer.

I'll leave generalising the Kronecker delta to a future PR. The only application I have in mind for this currently is for the identity matrix in #1965. The sum identities here allow us to show the identity matrix is a left and right identity.